/**                   GNU GENERAL PUBLIC LICENSE
 *                       Version 3, 29 June 2007
 *
 * Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
 * Everyone is permitted to copy and distribute verbatim copies
 * of this license document, but changing it is not allowed.
 * See License.txt file that comes with this distribution
 *
 *
 * Author: Vitaly German <vitaly.german@gmail.com>, (C) 2007-2008
 * 
 **/

#pragma once
#include <boost/shared_ptr.hpp>

#ifndef UNIX
#include<hash_map>
#else
#include <ext/hash_map>
#endif

#include "rlinear.h"
#ifdef UNIX
struct string_hash {
    size_t operator()(const std::string & s) const {
        __gnu_cxx::hash<char *> ch;
        return ch(s.c_str());
    }
};
typedef __gnu_cxx::hash_map<std::string, rfm_solver::Variable_ID, string_hash > Str2Var;
#endif

#ifndef UNIX
typedef stdext::hash_map<std::string, rfm_solver::Variable_ID > Str2Var;
#endif

using namespace rfm_solver;

class SolverEnv {
    Str2Var var_hash;
    Relation_aptr rel;
    Formula_aptr root;

    SolverEnv & operator =(const SolverEnv&);
    SolverEnv(const SolverEnv&);
public:
    SolverEnv(Relation_aptr rel1, Formula_aptr & root1)
            :rel(rel1), root(root1) {}
    SolverEnv(Relation_aptr rel1)
            :rel(rel1) {

        root = rel->add_and();
        rfm_solver::debug("\n+++F_And 1 created.\n");
#ifdef DEBUG
        rel->print();
#endif

    }
    Variable_ID get_variable (const std::string &  v);
    void update_variable (const Variable_ID & var, const std::string &  sv) {
        var_hash[sv] = var;
    }
    Relation_aptr & get_relation() {
        return rel;
    }
    Formula_aptr & get_root() {
        return root;
    }
    F_And_aptr get_root_F_And() {
        F_And_aptr res;
        if (root->get_type() == Op_And) {
            res = boost::dynamic_pointer_cast<F_And> (root);
        } else {
            rfm_solver::debug("+++F_And 2 created.");
            res = root->add_and();
            root = res;
        }
        return res;
    }
    void set_root(Formula_aptr r1) {
        root = r1;
    }
    ~SolverEnv() {
        rfm_solver::debug("+++~SolverEnv.");
    }
};

Variable_ID SolverEnv::get_variable (const std::string &  v) {
    Str2Var::iterator iv =  var_hash.find(v);
    Variable_ID var;
    if(iv!=var_hash.end()) {
        var = iv->second;
    } else {
        var = rel->declare_free(v);
        rfm_solver::debug("\n+++Variable", var, "declared.\n");
        var_hash[v] = var;
#ifdef DEBUG
        rel->print();
#endif

    }
    return var;
}

typedef boost::shared_ptr<SolverEnv> SolverEnv_aptr;
